(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)


include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".
include "bv/bv-lib.ma".


(*
lemma eq_op : ∀o1,o2.(eqb_op o1 o2=true) ↔ (o1=o2) .
#O1 #O2 elim O1 elim O2 %
normalize //
#A destruct qed.

lemma eq_op1 : ∀o1,o2.(eqb_op o1 o2=true) → o1=o2.
#O1 #O2 lapply (eq_op O1 O2)
*

 /2/ qed.

lemma eq_op2 : ∀o1,o2.o1=o2→ (eqb_op o1 o2=true).
#O1 #O2 lapply (eq_op O1 O2)
* /2/ qed.
*)



(* Given a list of structures l and an operator op
   create_struct_r replaces every occurrence of 
        lista op sub_l
   in l with
        sub_l                                           *) 
let rec create_struct_r (l:list struct) (op:operator) on l ≝
match l with [
  nil ⇒ [ ]
| cons h tl ⇒ match h with [
          lista sub_op sub_l ⇒ (if (eqb_op sub_op op) then sub_l else h::[])@(create_struct_r tl op)
        | _ ⇒ (h::[])@(create_struct_r tl op)]
].


definition create_struct  ≝λs. match s with [
  base t ⇒ base t 
| lista o l ⇒ lista o (create_struct_r l o)].


(* notation for atoms and unit. For example: «atom n»  with n ∈ ℕ , «unit» *)
(*notation "«x»" with precedence 70 
for @{(*create_struct*) ($x)}.*)



(*
theorem prova : 
  ∀o.∀l. (All ? (is_ass_norm_1_degree) l) →   is_ass_norm_1_degree (create_struct l o).
#O
elim O
  
  #L
  elim L (*Induco su L*)
    [1,3,5: // (*Se è vuota è banale*) 
    |2,4,6: 
      #H #TL #IND
      (*Forse mi serve parlare di append più che di cons*)
      lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
      (*Ora spezzo tutte le ipotesi*)
      #HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
      lapply (IND HIP2) -IND #IND 
      lapply HIP1 -HIP1
      elim H (*Induco sulla testa della lista così posso ridurre*)
        [1,3,5:
          #O2 #SUBL #HIP1
          normalize
          lapply HIP1 -HIP1
          (*Ora induco sul secondo operatore:fa esplodere abbastanza la dimostrazione*)
          elim O2 #HIP1           
          normalize
          (*Ora prendo le dimostrazioni con gli operatori uguali*)
          [1,5,9:           
            @All_append_r %
            [2,4,6:
              normalize in IND;
              //
            |1,3,5:
              normalize in HIP1; 
              lapply HIP1 -HIP1 * #HIP1 #T //
            ]
            (*Ora prendo le dimostrazioni con operatori diversi*)
            |2,3,4,6,7,8:  %
            [1,3,5,7,9,11: % #ABS destruct |2,4,6,8,10,12: // ]
          ] |2,4,6: #T #HIP1 @All_append_r % // 
      ]
   ]
qed.
*)



let rec is_ass_norm s ≝ match s with [
  lista op l ⇒ (All ? (neq_op_s op) l) ∧ (All ? is_ass_norm l)
| base t ⇒ True].

lemma append_cons_s : ∀A.∀a:A.∀l. a::l=[a]@l.
#A #a #L // qed.

lemma All_append_l : ∀A,P,l1,l2.
  All A P (l1 @ l2) → All A P l1 ∧ All A P l2.
  #A #P #L1 #L2 elim L1 normalize 
  [  /2/ ] 
  #H1 #H2 #H3 * #H4 #H5  %
  [ % [ @H4 | lapply (H3 H5) * #H6 #H7 @H6] | lapply (H3 H5) *#H9 #H10 @H10
  ] qed.
  
lemma All_append_r : ∀A,P,l1,l2. All A P l1 ∧ All A P l2 →   All A P (l1 @ l2).
  #A #P #L1 #L2 *
  elim L1 //
  #H #TL
  #IND  #HIP1 #HIP2
  normalize % normalize in HIP1; lapply HIP1 * #H12 #H13 /2/ qed.            

  





definition cs ≝λl.λo.lista o (create_struct_r l o).  
theorem create_struct_is_ass_norm: ∀o.∀l.All ? is_ass_norm l → is_ass_norm (cs l o).
(* following the previous theorem *)
  #O elim O #L elim L 
  [1,3,5:  
    normalize * %  //  
  |2,4,6:
    #H #TL #IND lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
    #HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
    lapply (IND HIP2) -IND #IND lapply HIP1 -HIP1 elim H 
    [1,3,5: 
     #T normalize * #T #T % 
      [1,3,5: % 
        [1,3,5: //
        |2,4,6: lapply IND normalize * //
        ]
      |2,4,6: %
        [1,3,5: //
        |2,4,6: lapply IND normalize * //] ]
      |2,4,6:  
      #O2 #SUBL #HIP1 normalize lapply HIP1 -HIP1 elim O2 #HIP1 normalize
      [1,5,9: 
        % @All_append_r % 
        [1,3,5,7,9,11: 
          lapply HIP1 normalize * -HIP1 * //
        |2,4,6,8,10,12: lapply IND normalize * //
        ]
      |2,3,4,6,7,8:% %  (* Qui le cose si moltiplicano più del dovuto, ma per ora mi accontento di
            saperle chiudere*)
        [1,5,9,13,17,21: % #ABS   destruct
        |2,4,6,8,10,12,14,16,18,20,22,24: lapply IND normalize * //
        |3,7,11,15,19,23: lapply HIP1 normalize * //
        ]
      ]     
    ]
  ]
qed.



(*
definition term1 ≝ 〚𝕒;𝕓;❨𝕓;𝕒❩〛.
definition term2 ≝ 〚𝕓;𝕒;❨𝕒;𝕓❩〛.

lemma prova : term1 ≡ term2. normalize 
@eqTrans [ @(lista par (list_swap ? [𝕒;𝕓;❨𝕓;𝕒❩] 0 1 (base unit)))]  // normalize  
 @eqContext1 // @eqContext // @eqSingleton 
normalize @eqTrans [ @(lista copar (list_swap ? [𝕓;𝕒] 0 1 (base unit))) ] //qed. *)

(*
let rec nth_s (s:struct) (g:list nat) (otherw: struct) on g ≝
match s with [
  lista op l ⇒ match g with [
      cons h tl ⇒ nth_s (nth h ? l otherw) tl otherw
    | nil ⇒ s
  ]
| base t ⇒ otherw  (* Or t, who knows?*)
].*)



lemma proviamo :  ∘⥤〚1+; 2+;2^;1^〛.



@(reduceTrans ? (〚1+;1^;2+;2^〛) ?) [ |@reduceEq @eqContext //
@eqTrans [ @(lista par (list_swap ? [2+;2^;1^] 0 1 (base unit))) ] @eqComm // normalize 
@eqTrans [ @(lista par (list_swap ? [1^;2+;2^] 0 2 (base unit))) ] @eqComm //]
@(reduceTrans ? (〚〚1+;1^〛;〚2+;2^〛〛) ? ) 
[ | @reduceEq  
@eqTrans [ @〚〚1+;1^〛;2+;2^〛  | @eqContext // @eqComm @eqAss //] 
@eqTrans [ @(〚1+;1^;2+;2^〛) | @eqComm 
@(eqAss ([1+;1^]) ? ?) // | // ] ]
@(reduceTrans ? (〚∘;∘〛) ?) [ 
@(reduceTrans ? (〚∘〛) ? ) [  @reduceEq @eqSingleton normalize // | 

@reduceEq @eqUnit normalize //]]
@reduceContext //  @reduceContext // qed.

    